ds:x:Id fp Type, da:k:Knd fp Type, es:ES, i:Id, e1, e2:{e:E| loc(e) = i }, L1,
L2:event-info(ds;da) List.
L1 = nil
 L2 = nil
 (x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 es-hist{i:l}(es;e1;e2) = (L1 @ L2)  event-info(ds;da) List
 e(e1,e2].es-hist{i:l}(es;e1;pred(e)) = L1 & es-hist{i:l}(es;e;e2) = L2 

latex

Definitions

b, P  Q, False, A, x:A. B(x), t  T, loc(e), Id, es-hist{i:l}(es;e1;e2), event-info(ds;da), P & Q, e(e1,e2].P(e), x. t(x), a:A fp B(a), Knd, ES, E, Prop, Top, IdDeq, f(x)?z, vartype(i;x), kind(e), KindDeq, valtype(e), as @ bs, [e, e'], {T}, SQType(T), ||as||, es-info(es;e), map(f;as), S  T, ij, pred(e), AB, , e  e' , P  Q, P  Q, A & B, (e <loc e'), 1of(t), x:A. B(x), (x  l), P  Q

Lemmas

map append sq, es-interval wf, general-append-cancellation, es-info wf, member-es-interval, list-subtype, subtype rel list, l member wf, map wf, es-interval-partition, es-locl wf, es-le wf, es-pred wf, es-le-loc, es-locl-iff, es-interval-non-zero, es-subinterval, pos length, length-map, length-append, length wf1, Id sq, es-interval wf2, append wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, not wf, event-info wf, es-E wf, es-loc wf, event system wf, Knd wf, fpf wf, Id wf, es-hist wf, es-loc-pred